The work concerns automatic generation of logical specifications fromrequirements models. Logical specifications obtained in such a way can besubjected to formal verification using deductive reasoning. Formal verificationconcerns correctness of a model behaviour. Reliability of the requirementsengineering is essential for all phases of software development processes.Deductive reasoning is an important alternative among other formal methods.However, logical specifications, considered as sets of temporal logic formulas,are difficult to specify manually by inexperienced users and this fact can beregarded as a significant obstacle to practical use of deduction-basedverification tools. A method of building requirements models using some UMLdiagrams, including their logical specifications, is presented step by step.Organizing activity diagrams into predefined workflow patterns enablesautomated extraction of logical specifications. The crucial aspect of thepresented approach is integrating the requirements engineering phase and theautomatic generation of logical specifications. A system of the deduction-basedverification is proposed. The reasoning process could be based on the semantictableaux method. A simple yet illustrative example of the requirementselicitation and verification is provided.
展开▼
